FindEquationalProof

FindEquationalProof[thm,axms] tries to find an equational proof of the symbolic theorem thm using the axioms axms.

FindEquationalProof[thm,"theory"] tries to find a proof of thm using the specified named axiomatic theory.

Please visit the official Wolfram Language Reference for more details and examples on core symbols.